Introducing some structure for model method bodies #3571

mattulbrich · 2025-02-23T21:55:56Z

Intended Change

This is a new feature request by users that wanted to use model methods.

The PR introduces method bodies that allow some statements. It is limited to

introducing local variables and variable assignment in method bodies.
introducing if-statements
return statements (as they have been there before)

This is still rather limited but allows you to structure your code already quite a bit.
The restrictions are:

Every if-branch-path must eventually contain a return statement (no phi-nodes)
Variables must be defined with var (due to a restriction in the lexer/parser)

The only thing that needs to be done is then to interpret these structures into a term.

My running example is the following which explains itself:

final class A {

    /*@ pure */
    int f(int x) {
        return 40-x;
    }
    
    /*@ model int maxF(int x, int y) {
      @   var x2 = f(x);
      @   var y2 = f(y);
      @   if(x2 > y2)
      @      return x2;
      @   else {
      @      return y2;
      @   }
      @ }
      @*/

    /*@ normal_behaviour
      @  ensures maxF(25, 30) == 15;
      @*/
    void test() { }

}

Plan

Implement the feature
Make sure we have consensus on wanting this

Type of pull request

New feature (non-breaking change which adds functionality)
There are changes to the (Java) code
Other: Changes to JML lexer and parser

Ensuring quality

I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
I added new test case(s) for new functionality.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

restricted to ifs and intermediate variables

and spotlessing

codecov · 2025-02-23T22:23:53Z

Codecov Report

Attention: Patch coverage is 34.61538% with 17 lines in your changes missing coverage. Please review.

Project coverage is 38.39%. Comparing base (284bb1e) to head (d616f00).
Report is 6 commits behind head on main.

Files with missing lines	Patch %	Lines
...java/de/uka/ilkd/key/speclang/njml/Translator.java	32.00%	14 Missing and 3 partials ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3571      +/-   ##
============================================
- Coverage     38.39%   38.39%   -0.01%     
- Complexity    17238    17239       +1     
============================================
  Files          2098     2098              
  Lines        127324   127346      +22     
  Branches      21442    21444       +2     
============================================
+ Hits          48886    48891       +5     
- Misses        72427    72441      +14     
- Partials       6011     6014       +3

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

wadoon · 2025-02-23T23:58:53Z

My questions would also be:

Why keep it limited to if statements? In jmlparser all Java/JML-constructs are allowed.
Does pure require termination?

Maybe we should add a jmlFrame : { } (in contrast to method-frame: {}) to allow more statements, and also have a different execution semantics.

mattulbrich · 2025-02-24T09:47:00Z

My questions would also be:
Why keep it limited to if statements? In jmlparser all Java/JML-constructs are allowed.

Because thus jml model method bodies can remain purely logical expressions and their definition can be directly expanded into the sequent. That is a fundamental asset of model methods as they are implemented in KeY (like related constructs in other verification frameworks). Dealing with loops in particular would make this impossible.

This was driven by trying to relax notation while keeping the verification-system power of the type definitions.

How does the JavaDL-definition axiom or taclet for model methods look like in jmlparser?

Does pure require termination?

I think actually, it does. In KeY, however, the expansion mechanism for non-model methods, is conservative and uses [] box-semantics to be on the safe side.

Maybe we should add a jmlFrame : { } (in contrast to method-frame: {}) to allow more statements, and also have a different execution semantics.

I would refrain from putting jml model methods into modalities, It's their power to define functions directly.

I would be happy to intrdoduce ghost methods that can use any code. They do not even need to be pure.
ghost loops/ifs in regular methods would also be really cool.

wadoon · 2025-02-25T15:34:49Z

key.core/src/main/antlr4/JmlLexer.g4

@@ -7,6 +7,8 @@ lexer grammar JmlLexer;
   // needed for double literals and ".."
   private int _lex_pos;

+   private boolean parensEndExpr = false;


I think we reached a point in which we should rather rewrite the lexer w/o using modes for top-level and expr-mode.

I wonder if these modes are really necessary in the lexer.

Yes one could name a variable "ensures", and write ensures ensures > 4;. But this is fully confusing.
I would be in favour of allowing backticks in these cases for turning keywords into identifiers.

As I did this, I came from the jmllang lexer/parser (Java+JML in ANTLR), where I used this heavily.

The advantage is, that the error messages are a little bit better. ("Expected identifier" vs "Expected identifier, ensures, requires, ... "). But the price is a complicated lexer.

I would now get rid of it, and introduce a grammar rule:

identifier: IDENTIFIER | MODEL | ENSURES | REQUIRES | ...;

I would keep modes for Strings & Co.

Do we not have (proposed) backticks for JavaDL escape of complete terms?

Do we not have (proposed) backticks for JavaDL escape of complete terms?

Maybe, don't know. Was that not (* ... *) ?

Actually I even actively avoid ensures ensures > 4; to be legal.
Escaping the identifier ensures seems like a natural thing to do.
Languages like SMT, SQL, ... have support for this, with explicit escapes.
(I had it in ivil, too. It was a simple addition to the parser.)

While it is a discussion worth having, it is beyond this PR that will have to accommodate to the current parser framework; and does so with not so much extra overhead.
(Just that an extra ")" leads back to toplevel mode if that is enabled -- this condition might probably even be dropped, but I wanted to be conservative.)

Not so complicated: #3572

Apparently we do not show these long "expected ....." lists anyway in our syntax error to string conversion anyway, so this may work well (eventually).

wadoon · 2025-02-25T15:36:05Z

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java

+            String name = varCtx.IDENT().getText();
+            SLExpression expr = accept(varCtx.expression());
+            Term term = expr.getTerm();
+            LogicVariable logVar = new LogicVariable(new Name(name), term.sort());


What happens on a name clash?

var x = 1; var x = 2;

Yeah. This is currently allowed. You can write var x = 1; x = 2; which should be legal.

It would be nicer to ensure:

If keyword "var" is present, no variable x must be in namespace

If no keyword var is present, there is a variable x of compatible type present in the namespace.

It is not required technically, and everything is welldefined in either case. But it would violate Java principles.

Will add this.

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java

introducing model methods with bodies

a312ab4

restricted to ifs and intermediate variables

mattulbrich added JML Parser Feature New feature or request Review Request Waiting for review labels Feb 23, 2025

mattulbrich self-assigned this Feb 23, 2025

mattulbrich requested review from WolframPfeifer and wadoon February 23, 2025 21:58

Allowing variables to be reassigned.

d616f00

and spotlessing

wadoon reviewed Feb 25, 2025

View reviewed changes

mattulbrich marked this pull request as draft February 27, 2025 00:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Introducing some structure for model method bodies #3571

Introducing some structure for model method bodies #3571

mattulbrich commented Feb 23, 2025

codecov bot commented Feb 23, 2025 •

edited

Loading

wadoon commented Feb 23, 2025

mattulbrich commented Feb 24, 2025 •

edited

Loading

wadoon Feb 25, 2025

mattulbrich Feb 27, 2025

wadoon Feb 27, 2025

mattulbrich Feb 27, 2025

wadoon Feb 27, 2025

mattulbrich Feb 27, 2025

wadoon Feb 25, 2025

mattulbrich Feb 27, 2025

mattulbrich Feb 27, 2025

Introducing some structure for model method bodies #3571

Are you sure you want to change the base?

Introducing some structure for model method bodies #3571

Conversation

mattulbrich commented Feb 23, 2025

Intended Change

Plan

Type of pull request

Ensuring quality

Additional information and contact(s)

codecov bot commented Feb 23, 2025 • edited Loading

Codecov Report

wadoon commented Feb 23, 2025

mattulbrich commented Feb 24, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov bot commented Feb 23, 2025 •

edited

Loading

mattulbrich commented Feb 24, 2025 •

edited

Loading